es:ES, e:E. loc(es-init(es;e)) ~ loc(e) 

latex

Definitions	t  T, x:A. B(x), b, Void, x:AB(x), P  Q, False, A, x:AB(x), ES, A/x,y. B(x;y), 1of(t), E, left+right, P  Q, True, P  Q, P & Q, P  Q, loc(e), <a,b>, Id, s = t, {T}, SQType(T), s ~ t, es-init(es;e), e  e'
Lemmas	Id sq, es-E wf, event system wf, es-init-le, es-le-loc, es-loc-pred, es-init wf